the_w:World.
FairFifo
 (e:E.
 (isrcv(kind(e)))
  (sends(lnk(kind(e));sender(e))[index(e)]
  (=
  (msg(lnk(kind(e));tag(kind(e));val(e))
  ( Msg(the_w.M))) 

latex

Definitions	t  T, x:A. B(x), FairFifo, x:AB(x), E, b, w.M, Msg(M), s = t, P  Q, World, A  B, P & Q, i  j < k, {x:A| B(x)} , x:A  B(x), False, A, , sender(e), index(e), {T}, isrcv(k), val(e), msg(l;t;v), Msg, sends(l;e), l[i], kind(e), lnk(k), source(l), <a, b>, time(e), s ~ t, match(l;t;t'), x.A(x), mu(f), , #$n, {i..j}, x:A. B(x), loc(e), act(e), msg(a)
Lemmas	w-match-property, isrcv wf, w-E wf, w-match-exists, mu-property, mu wf, le wf, assert wf, w-match wf, lnk wf, w-ekind wf, w-time wf, nat wf, world wf, fair-fifo wf